g, h:GrpSig, f:MonHom(g,h). Inj(|g|;|h|;f)  Ident(|h|;*;e)  Ident(|g|;*;e) 

latex

Up	groups 1
Definitions of Statement	IsMonHom{M1,M2}(f), MonHom(M1,M2)
Definitions	t  T, Ident(T;op;id), P  Q, x:A. B(x), P  Q, P  Q, P & Q, x f y, FunThru2op(A;B;opa;opb;f), IsMonHom{M1,M2}(f), Inj(A;B;f), MonHom(M1,M2),
Lemmas	grp sig wf, monoid hom wf, inject wf, grp id wf, grp op wf, ident wf, grp car wf, monoid hom properties